Library ceva_conjugate
Require Export PointsType.
Require Import TrianglesDefs.
Require Import incidence.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Require Import TrianglesDefs.
Require Import incidence.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
The P-Ceva conjugate of Q is the perspector of the cevian triangle of P and anti-cevian
triangle of Q
Definition ceva_conjugate P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
cTriple (u*(-q×r×u+r×p×v+p×q×w)) (v*(q×r×u-r×p×v+p×q×w)) (w*(q×r×u+r×p×v-p×q×w))
end.
Definition is_ceva_conjugate P Q R := eq_points P (ceva_conjugate Q R).
Lemma ceva_conjugate_property :
∀ P Q,
is_perspector (ceva_conjugate P Q) (cevian_triangle P) (anti_cevian_triangle Q).
Proof.
intros.
destruct P.
destruct Q.
unfold is_perspector.
unfold ceva_conjugate, col.
simpl.
repeat split;ring.
Qed.
End Triangle.